#형식 검증

테렌스 타오: AI가 수학계 최초의 분업을 이끌 수 있다

천재 수학자 테렌스 타오는 AI가 수학 연구에 역사상 처음으로 '분업'을 도입할 수 있다고 주장합니다. 기존의 수학자들은 문제 설정부터 검증, 논문 작성까지 모든 것을 혼자 해야 했지만, 형식 검증 등 AI 기술의 도움으로 대규모 팀 간의 전문적 협업이 가능해진다는 것입니다. 다만, 인간의 통찰력과 엄격한 검증이 뒷받침될 때만 AI가 온전한 잠재력을 발휘할 수 있다고 강조하며 수학 연구의 패러다임 전환을 예고했습니다.

LLM이 실제 시스템을 정확히 모델링할 수 있을까?

최신 LLM들이 동시성 및 분산 시스템 명세 언어인 TLA+를 사용해 시스템을 모델링하는 역량을 평가한 연구 결과입니다. 연구진이 개발한 자동화 벤치마크 'SysMoBench'에 따르면, 최신 LLM들은 문법이나 기본 실행 단계에서는 거의 완벽한 점수를 기록했지만, 실제 코드와 모델이 일치하는지 검증하는 단계(46%)와 핵심 속성을 만족하는지 확인하는 단계(41%)에서는 대폭 실패했습니다. 이는 현재 AI가 시스템 코드의 실제 구조를 추상화해 정확한 형식 모델을 작성하기보다는, 학습 데이터에 존재하는 교과서적인 예제를 단순히 암기하여 재생산하는 한계를 명확히 보여줍니다.